\begin{tabbing}
$\forall$\=$P$, $Q$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $X$:es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)), $Y$:es{-}real\{i:l\}(${\it es}$.$Q$(${\it es}$)),\+
\\[0ex]$p$:R{-}compat\=\{i:l\}\+
\\[0ex](1of($X$); 1of($Y$)).
\-\-\\[0ex]es{-}real{-}and\{i:l\}($P$; $Q$; $X$; $Y$; $p$) $\in$ es{-}real\{i:l\}(${\it es}$.($P$(${\it es}$) \& $Q$(${\it es}$)))
\end{tabbing}